﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace Logic
{
	class SATSolver
	{
		class Model
		{
			public CNFSentence Sentence;
			public int[] AssignedValues;
			public List<int> UnassignedVarIndexes;
			public List<int> UndeterminedClauses;
			public int[] UnassignedNumValuesInClause;
			//TODO: neg and pos index copy for finding pure symbols

			public Model()
			{
			}

			public Model(CNFSentence sentence)
			{
				Sentence = sentence;
                
				AssignedValues = new int[sentence.LogicalSystem.Symbols.Count];
				UnassignedVarIndexes = new List<int>(sentence.VariableIndex.Keys);
				//Linked list?
				UndeterminedClauses = Enumerable.Range(0, sentence.Formula.Count).ToList();				
				UnassignedNumValuesInClause = sentence.Formula.Select(x => x.Count).ToArray();
			}

			public Model Copy()
			{
				Model c = new Model();
				c.Sentence = this.Sentence;
				c.AssignedValues = new int[this.AssignedValues.Length];
				c.UnassignedNumValuesInClause = new int[this.UnassignedNumValuesInClause.Length];
				c.UnassignedVarIndexes = new List<int>(this.UnassignedVarIndexes);
				Array.Copy(this.AssignedValues, c.AssignedValues, this.AssignedValues.Length);
				Array.Copy(this.UnassignedNumValuesInClause, c.UnassignedNumValuesInClause, this.UnassignedNumValuesInClause.Length);
				c.UndeterminedClauses = new List<int>(this.UndeterminedClauses);

				return c;
			}
		}

		Model solutionModel;
		int maxDepth;
        int[] precedence = null;
		public int NodesExpanded;
        Random rand;

        public SATSolver()
        {
            rand = new Random();
        }

        //TODO: try to use component split
		public int[] Solve(CNFSentence sentence, int[] oldSolutionForPrecedence = null)
		{            
			NodesExpanded = 0;
			maxDepth = 0;

			if (sentence.AlwaysTrueOrFalse == false)
				return null;
			Model model = new Model(sentence);
			if (sentence.AlwaysTrueOrFalse == true)
				return model.AssignedValues;

            precedence = oldSolutionForPrecedence;

			List<int> unitClauses = new List<int>();
			for (int i = 0; i < sentence.Formula.Count; i++)			
				if (sentence.Formula[i].Count == 1) unitClauses.Add(i);
			
			
			bool solved = Solve(model, unitClauses);
			if (solved)
				return solutionModel.AssignedValues;
			return null;
		}

		bool Solve(Model model, List<int> unitClauses)
		{
			NodesExpanded++;

            for (int i = 0; i < unitClauses.Count; i++)
            {
                if (!model.UndeterminedClauses.Contains(unitClauses[i])) continue; //assigning one unit clause can render unit clauses ahead with the same variable as assigned
                NodesExpanded++;
                //TODO: optimize this
                List<int> unitClause = model.Sentence.Formula[unitClauses[i]];
                int v = 0;
                for (int k = 0; k < unitClause.Count; k++)
                {
                    v = unitClause[k];
                    int vv = v;
                    if (vv < 0) vv = ~vv;
                    if (model.UnassignedVarIndexes.Contains(vv)) break;
                }


                bool neg = false;
                if (v < 0) { v = ~v; neg = true; }
                List<int> newUnitClauses;
                bool? result = Assign(model, v, !neg, out newUnitClauses);
                if (result != null) return result.Value;
                unitClauses.AddRange(newUnitClauses);
            }

			//TODO: use pure variable heuristic
			//TODO: use degree heuristic (variable, that appears in max number of clauses)
			int nextSymbol = model.UnassignedVarIndexes.First();

			
            
            bool[] prec;
            if(rand.Next() < 0.5)
                prec = new[] { true, false };
            else
                prec = new[] { false, true };
            //Strangely caching old solution doesn't help at all
            //if (precedence != null && precedence[nextSymbol] != 0)
            //{
            //    prec[0] = precedence[nextSymbol] == 1;
            //    prec[1] = !prec[0];
            //}

			List<int> newuc;
			Model newModel1 = model.Copy();
			bool? res = Assign(newModel1, nextSymbol, prec[0], out newuc);
			if (res == null) res = Solve(newModel1, newuc);
			if (res == true) return true;
			

			Model newModel2 = model.Copy();
			res = Assign(newModel2, nextSymbol, prec[1], out newuc);
			if (res == true) return true;
			if (res == null) return Solve(newModel2, newuc);
			return false;
		}
  
		bool? Assign(Model model, int symbol, bool value, out List<int> newUnitClauses)
		{
			newUnitClauses = new List<int>();
			model.AssignedValues[symbol] = value ? 1 : -1;
			if (!model.UnassignedVarIndexes.Contains(symbol))
				throw new Exception();
			model.UnassignedVarIndexes.Remove(symbol);
            List<int> clausesIn = model.Sentence.VariableIndex[symbol].ClausesIn;
			if (!value) symbol = ~symbol;

			for (int i = 0; i < clausesIn.Count; i++)
			{
				int clauseIndex = clausesIn[i];
                //TODO: hot line here
                int undeterIndex = model.UndeterminedClauses.IndexOf(clauseIndex);
                if (undeterIndex == -1) continue;

				List<int> clause = model.Sentence.Formula[clauseIndex];			
				for (int j = 0; j < clause.Count; j++)
				{
					if (clause[j] == symbol) //appears as positive (or negative, and we're assigning negative), clause is true
					{						
						model.UndeterminedClauses.RemoveAt(undeterIndex);						
						if (model.UndeterminedClauses.Count == 0) //every clause is true - success
						{
							solutionModel = model;
							return true;
						}
						i--;						
						break;
					}

					if (clause[j] == ~symbol) //appears as negative (or positive, and we're assigning negative)
					{
						model.UnassignedNumValuesInClause[clauseIndex]--;
						if (model.UnassignedNumValuesInClause[clauseIndex] == 0) //all negatives, clause is false, terminate						
							return false;
						if (model.UnassignedNumValuesInClause[clauseIndex] == 1)
							newUnitClauses.Add(clauseIndex);						
					}
				}
			}
			
			return null;
		}

		public bool CheckSolution(CNFSentence sentence, int[] result)
		{
			for (int i = 0; i < sentence.Formula.Count; i++)
			{
				List<int> clause = sentence.Formula[i];
				bool istrue = false;
				for (int j = 0; j < clause.Count; j++)
				{
					int literal = clause[j];
					bool neg = false;
					if (literal < 0)
					{
						neg = true;
						literal = ~literal;
					}

					int val = result[literal];
					if (val == 1 && !neg || val == -1 && neg)
					{
						istrue = true;
						break;
					}
				}

				if (!istrue) 
					return false;
			}

			return true;
		}
	}
}
